Add German cache-coherence protocol example (Murphi > TLA+)#214
Open
lemmy wants to merge 3 commits into
Open
Conversation
A new specifications/GermanProtocol directory translating the German
directory-based cache-coherence protocol from the Murphi sources in
Divjyot Sethi's ProtocolDeadlockFiles repository (provenance: German ->
Chou/Mannava/Park FMCAD 2004 -> Sethi/Talupur/Malik ATVA 2014). The TLA+
was synthesized by Opus 4.8 under supervision; see the directory README.md
for the full attribution chain.
Three levels of refinement, each a standalone module:
- GermanCoherence: control-only model, coherence/mutual exclusion only.
- German: the CMP-style parameterized abstraction (concrete nodes plus
a single abstract "Other" environment node and the ABS_* rules).
- GermanWithMutex: the data-carrying refinement, adding data-integrity
(DataProp), the structural well-formedness invariants, and the
Lemma_1/Lemma_2 noninterference lemmas, plus liveness under fairness.
Tooling added for each spec, following the conventions already used in
the repo (INSTANCE-based Apalache wrappers; MC* TLC drivers):
- AP{GermanCoherence,German,GermanWithMutex}.tla/.cfg apply Apalache
type annotations via INSTANCE so the specs stay tool-agnostic; nodes
and data are uninterpreted types so the NODE \cup {Other, NoNode}
unions type-check. Safety invariants only (no liveness).
- MC{GermanCoherence,German,GermanWithMutex}.tla/.cfg use the smallest
meaningful constants -- two nodes (the minimum for non-vacuous mutual
exclusion) and, for GermanWithMutex, two data values (so writes are
distinguishable) -- with Permutations symmetry reduction.
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Explain that the \A j conjunct in the ABS_RecvInvAck action's enabling condition is the operational mutual-exclusion noninterference lemma (Chou/Mannava/Park FMCAD 2004; Sethi/Talupur/Malik arXiv:1407.7468): germanWithMutex.m conjoins it, germanNoMutex.m deliberately omits it. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
These specs were translated from Murphi, whose rules cannot express
intra-action nondeterminism, so a single nondeterministic choice must be
split across separate rules. TLA+ expresses that choice directly with
existential quantification and disjunction, so collapse each flavour-split
pair into one action. This removes the duplication the Murphi encoding
forced without changing the specs' behaviors.
Verified equivalence-preserving with TLAPS: an auxiliary module per spec
keeps the old split actions as _o operators, and TLAPS proves
Next <=> Next_o (one BY DEF biconditional lemma per merged action).
```tla
(* Per-action equivalences (divide and conquer). *)
LEMMA SendReqEquiv ==
ASSUME NEW i \in NODE
PROVE SendReq(i) <=> (SendReqS_o(i) \/ SendReqE_o(i))
BY DEF SendReq, SendReqS_o, SendReqE_o
LEMMA RecvReqEquiv ==
ASSUME NEW i \in NODE
PROVE RecvReq(i) <=> (RecvReqS_o(i) \/ RecvReqE_o(i))
BY DEF RecvReq, RecvReqS_o, RecvReqE_o
LEMMA SendGntEquiv ==
ASSUME NEW i \in NODE
PROVE SendGnt(i) <=> (SendGntS_o(i) \/ SendGntE_o(i))
BY DEF SendGnt, SendGntS_o, SendGntE_o
LEMMA RecvGntEquiv ==
ASSUME NEW i \in NODE
PROVE RecvGnt(i) <=> (RecvGntS_o(i) \/ RecvGntE_o(i))
BY DEF RecvGnt, RecvGntS_o, RecvGntE_o
-------------------------------------------------------------------------------
(* Coarse-grained equivalence at the level of Next. *)
THEOREM NextEquiv == Next <=> Next_o
BY SendReqEquiv, RecvReqEquiv, SendGntEquiv, RecvGntEquiv
DEF Next, Next_o
```
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
muenchnerkindl
approved these changes
Jul 20, 2026
muenchnerkindl
left a comment
muenchnerkindl
left a comment
Collaborator
There was a problem hiding this comment.
A nice addition to the examples repository!
| /\ curCmd # "Empty" | ||
| /\ chan3' = [chan3 EXCEPT ![i] = "Empty"] | ||
| /\ shrSet' = [shrSet EXCEPT ![i] = FALSE] | ||
| /\ exGntd' = IF exGntd = TRUE THEN FALSE ELSE exGntd |
| /\ chan1 \in [NODE -> MsgCmd] | ||
| /\ chan2 \in [NODE -> MsgCmd] | ||
| /\ chan3 \in [NODE -> MsgCmd] | ||
| /\ invSet \in [NODE -> BOOLEAN] |
Collaborator
There was a problem hiding this comment.
Wouldn't it be more idiomatic to represent invest and shrSet as sets rather than as boolean-valued functions? (But perhaps you prefer leaving them as they are in order to stay as close as possible to the original Murphi model?)
| Lemma_1 == | ||
| \A i \in NODE : | ||
| (chan3[i] = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => | ||
| \A j \in NODE : |
Collaborator
There was a problem hiding this comment.
Consider writing \A j \in Node \ {i}
| @@ -0,0 +1,175 @@ | |||
| -------------------------------- MODULE German -------------------------------- | |||
Collaborator
There was a problem hiding this comment.
Throughout the module, some comments / explanations would be nice. There is a comment for one of the actions but that's it. I understand that the README points to relevant background, though.
|
|
||
| ------------------------------------------------------------------------------- | ||
|
|
||
| ABS_RecvReq == |
Collaborator
There was a problem hiding this comment.
I am assuming that ABS stands for "abstract" but in what sense?
| \A i \in NODE : | ||
| cache[i].state = "E" => | ||
| /\ exGntd = TRUE | ||
| /\ \A j \in NODE : |
Collaborator
There was a problem hiding this comment.
\A j \in NODE \ {i} : ?
| \A i \in NODE : | ||
| (chan3[i].cmd = "InvAck" /\ curCmd # "Empty" /\ exGntd = TRUE) => | ||
| /\ chan3[i].data = auxData | ||
| /\ \A j \in NODE : |
| @@ -0,0 +1,4 @@ | |||
| ------------------------- MODULE MCGermanWithMutex ------------------------- | |||
| EXTENDS GermanWithMutex | |||
|
|
|||
| @@ -0,0 +1,241 @@ | |||
| ----------------------------- MODULE GermanWithMutex ----------------------------- | |||
Collaborator
There was a problem hiding this comment.
Explain the relationship with the other specs here? I understand that it also represents data whereas GermanCoherence only considers control state, but why "with mutex"?
| @@ -0,0 +1,44 @@ | |||
| ----------------------------- MODULE APGerman ----------------------------- | |||
Collaborator
There was a problem hiding this comment.
Here or elsewhere, indicate the command line used for running Apalache? (I am assuming you are using the default bound of 10 states for bounded model checking?)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds an example translated from Divjyot Sethi's Murphi sources, with three refinement levels:
Other+ABS_*rules)DataProp, invariants, noninterference lemmas, and liveness under fairnessEach spec ships with TLC and Apalache models/configs following existing repo conventions.